Library PointsType

Require Export Reals.
Open Scope R_scope.

Record Triple : Set :=
    cTriple
    {
        X : R;
        Y : R;
        Z : R
    }.

Class triangle_theory := {
 a:R;
 b:R;
 c:R;
 apos: a > 0;
 bpos: b > 0;
 cpos: c > 0;
 ineq_1 : a + b - c >0;
 ineq_2 : a - b + c >0;
 ineq_3 : -a + b + c >0
}.

Definition pointA := cTriple 1 0 0.
Definition pointB := cTriple 0 1 0.
Definition pointC := cTriple 0 0 1.

Definition eq_points P Q :=
 X(Q)×Y(P) = X(P)×Y(Q) ∧ X(Q)×Z(P) = X(P)×Z(Q).

Definition eq_triangles T1 T2 :=
 match T1,T2 with
  (X,Y,Z), (U,V,W) ⇒ eq_points X U ∧ eq_points Y V ∧ eq_points Z W
 end.

Definition is_not_on_sidelines P :=
 match P with
  cTriple X Y Z ⇒ X≠0 ∧ Y≠0 ∧ Z≠0
 end.

Lemma a_not_zero : ∀ `{M:triangle_theory}, a≠0.
Proof.
intros.
assert (T:=apos).
auto with real.
Qed.

Lemma b_not_zero : ∀ `{M:triangle_theory}, b≠0.
Proof.
intros.
assert (T:=bpos).
auto with real.
Qed.

Lemma c_not_zero : ∀ `{M:triangle_theory}, c≠0.
Proof.
intros.
assert (T:=cpos).
auto with real.
Qed.

Hint Resolve a_not_zero b_not_zero c_not_zero : triangle_hyps.